IrrelevantFamilyIndex.agda:26,9-10
Variable n is declared irrelevant, so it cannot be used here
when checking that the expression n has type Nat
